Nuprl Lemma : append-nil
11,40
postcript
pdf
l
:(top List). sqequal(append(
l
; []);
l
)
latex
Definitions
x
:
A
.
B
(
x
)
,
append(
as
;
bs
)
,
Y
,
t
T
Lemmas
top
wf
origin
l:(top List). sqequal(append(l; []); l) l:(top List). sqequal(append(l; []); l) x:A. B(x)
T